Skip to content

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Feb 6, 2026

This PR adds support for dot syntax in ghost variables and states while keeping it backward compatible with the previous syntax. For this, a new non-terminal dotCall was added to the grammar and implemented in the AST visitor.

Currently, all of these are equivalent: size(this), this.size(), and size(). To refer to the previous value of size, we can either use size(old(this)) or old(this).size.

In the future, we plan to drop the functional syntax and only keep the dot syntax to avoid ambiguity and confusion.

Example

@Ghost("int n")
public class CorrectDotNotationIncrementOnce {

    // explicit this
    @StateRefinement(to="this.n() == 0")
    public CorrectDotNotationIncrementOnce() {}

    // implicit this
    @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
    public void incrementOnce() {}
}

@rcosta358 rcosta358 self-assigned this Feb 6, 2026
@rcosta358 rcosta358 added the enhancement New feature or request label Feb 6, 2026
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

couple changes

}

private Expression dotCallCreate(DotCallContext rc) throws LJError {
if (rc.OBJECT_TYPE() != null) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

there are a couple more cases here right?
OBJECT_TYPE actually accepts multiple fields like this.a.b so there could be several indexes of . maybe we can send an error if that happens since we dont allow refering to field chains (yet at least) but we shouldn't just ignore it

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep!

String simpleName = text.substring(dot + 1);
String name = Utils.qualifyName(prefix, simpleName);
List<Expression> args = getArgs(rc.args(0));
if (!args.isEmpty() && args.get(0)instanceof Var v && v.getName().equals(Keys.THIS)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

picky space betwee args.get(0) and instanceof

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I also don't like it, blame the formatter 😂

}
}

private Expression dotCallCreate(DotCallContext rc) throws LJError {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We def need documentation here explaining what the function does

Copy link
Collaborator Author

@rcosta358 rcosta358 Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should I add documentation for all other functions in this file then?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

probably a good idea yeah

throw new SyntaxError("Cannot use both dot notation and explicit 'this' argument. Use either 'this."
+ simpleName + "()' or '" + simpleName + "(this)'", text);

args.add(0, new Var(target));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

add comment here saying this transforms the call this.func to be used internally as func(this)

List<Expression> targetArgs = getArgs(rc.args(0));
List<Expression> funcArgs = getArgs(rc.args(1));
funcArgs.add(0, new FunctionInvocation(targetFunc, targetArgs));
return new FunctionInvocation(name, funcArgs);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

also add comment here saying what the transformation is

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

niceee

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants